(set-logic QF_LRA)
(set-info :source |CPAchecker with k-induction on SV-COMP14 program using MathSAT5, submitted by Philipp Wendler, http://cpachecker.sosy-lab.org|)
(set-info :smt-lib-version 2.0)
(set-info :category "industrial")

(define-fun _1 () Bool true)
(declare-fun busy@1 () Real)
(declare-fun __ADDRESS_OF_virtio_rng_driver () Real)
(declare-fun |main::tmp___1@3| () Real)
(declare-fun ldv_mutex@1 () Real)
(declare-fun |main::__cil_tmp10@1| () Real)
(declare-fun |main::tmp___1@2| () Real)
(declare-fun |main::__cil_tmp10@3| () Real)
(declare-fun __ADDRESS_OF_have_data () Real)
(declare-fun |main::ldv_s_virtio_rng_driver_virtio_driver@1| () Real)
(declare-fun |main::__cil_tmp10@2| () Real)
(declare-fun |main::tmp___0@2| () Real)
(define-fun _7 () Real 0)
(define-fun _36 () Real (- 1))
(define-fun _46 () Real __ADDRESS_OF_have_data)
(define-fun _72 () Real (- 40))
(define-fun _73 () Bool (<= _46 _72))
(define-fun _74 () Bool (not _73))
(define-fun _81 () Real __ADDRESS_OF_virtio_rng_driver)
(define-fun _89 () Real (* (- 1) _81))
(define-fun _105 () Real 1)
(define-fun _169 () Real |main::tmp___1@3|)
(define-fun _170 () Bool (= _169 _7))
(define-fun _176 () Real |main::__cil_tmp10@3|)
(define-fun _179 () Bool (= _176 _7))
(define-fun _182 () Bool (not _179))
(define-fun _191 () Real |main::__cil_tmp10@2|)
(define-fun _196 () Real |main::tmp___1@2|)
(define-fun _237 () Bool (= _196 _7))
(define-fun _239 () Bool (not _237))
(define-fun _240 () Real |main::ldv_s_virtio_rng_driver_virtio_driver@1|)
(define-fun _241 () Bool (= _240 _7))
(define-fun _242 () Real (ite _241 _105 _7))
(define-fun _243 () Bool (= _191 _242))
(define-fun _244 () Bool (and _237 _243))
(define-fun _245 () Bool (= _191 _7))
(define-fun _247 () Bool (and _244 _245))
(define-fun _250 () Real |main::__cil_tmp10@1|)
(define-fun _251 () Bool (= _191 _250))
(define-fun _252 () Bool (and _239 _251))
(define-fun _253 () Bool (or _247 _252))
(define-fun _254 () Real |main::tmp___0@2|)
(define-fun _255 () Bool (= _254 _7))
(define-fun _257 () Bool (and _253 _255))
(define-fun _263 () Real ldv_mutex@1)
(define-fun _264 () Bool (= _263 _105))
(define-fun _267 () Bool (not _264))
(define-fun _270 () Real busy@1)
(define-fun _271 () Bool (= _270 _7))
(define-fun _273 () Bool (and _257 _271))
(define-fun _274 () Bool (not _271))
(define-fun _275 () Bool (and _257 _274))
(define-fun _276 () Bool (<= _46 _7))
(define-fun _277 () Bool (not _276))
(define-fun _279 () Bool (and _275 _277))
(define-fun _280 () Bool (or _273 _279))
(define-fun _281 () Bool (and _170 _280))
(define-fun _283 () Bool (= _176 _242))
(define-fun _284 () Bool (and _281 _283))
(define-fun _300 () Real (+ _46 _89))
(define-fun _301 () Bool (<= _300 _72))
(define-fun _302 () Bool (and _74 _301))
(define-fun _315 () Bool (and _182 _302))
(define-fun _317 () Bool (and _267 _315))
(define-fun _318 () Bool (not _317))
(define-fun _319 () Bool (not _284))
(define-fun _320 () Bool (or _318 _319))
(define-fun _321 () Bool (not _320))
(declare-fun |main::__cil_tmp10@4| () Real)
(declare-fun |main::tmp___0@3| () Real)
(declare-fun |main::tmp___1@4| () Real)
(define-fun _173 () Bool (not _170))
(define-fun _184 () Real |main::tmp___0@3|)
(define-fun _185 () Bool (= _184 _7))
(define-fun _192 () Bool (= _176 _191))
(define-fun _282 () Bool (and _173 _280))
(define-fun _285 () Bool (and _179 _284))
(define-fun _296 () Bool (and _192 _282))
(define-fun _297 () Bool (or _285 _296))
(define-fun _298 () Bool (and _185 _297))
(define-fun _312 () Bool (and _271 _298))
(define-fun _313 () Bool (and _274 _298))
(define-fun _314 () Bool (or _312 _313))
(define-fun _329 () Real |main::tmp___1@4|)
(define-fun _330 () Bool (= _329 _7))
(define-fun _363 () Bool (and _314 _330))
(define-fun _365 () Real |main::__cil_tmp10@4|)
(define-fun _366 () Bool (= _242 _365))
(define-fun _367 () Bool (and _363 _366))
(define-fun _368 () Bool (= _365 _7))
(define-fun _371 () Bool (not _368))
(define-fun _402 () Bool (and _302 _371))
(define-fun _404 () Bool (and _267 _402))
(define-fun _405 () Bool (not _404))
(define-fun _406 () Bool (not _367))
(define-fun _407 () Bool (or _405 _406))
(define-fun _408 () Bool (not _407))

(push 1)
(assert _1)
(push 1)
(assert _321)
;(set-info :status sat)
(check-sat)
(pop 1)
(push 1)
(assert _408)
;(set-info :status sat)
(check-sat)

